/*
 * Atomic Predicates for Transformers
 * 
 * Copyright (c) 2015 UNIVERSITY OF TEXAS AUSTIN. All rights reserved. Developed
 * by: HONGKUN YANG and SIMON S. LAM http://www.cs.utexas.edu/users/lam/NRL/
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * with the Software without restriction, including without limitation the
 * rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
 * sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * 1. Redistributions of source code must retain the above copyright notice,
 * this list of conditions and the following disclaimers.
 * 
 * 2. Redistributions in binary form must reproduce the above copyright notice,
 * this list of conditions and the following disclaimers in the documentation
 * and/or other materials provided with the distribution.
 * 
 * 3. Neither the name of the UNIVERSITY OF TEXAS AUSTIN nor the names of the
 * developers may be used to endorse or promote products derived from this
 * Software without specific prior written permission.
 * 
 * 4. Any report or paper describing results derived from using any part of this
 * Software must cite the following publication of the developers: Hongkun Yang
 * and Simon S. Lam, Scalable Verification of Networks With Packet Transformers
 * Using Atomic Predicates, IEEE/ACM Transactions on Networking, October 2017,
 * Volume 25, No. 5, pages 2900-2915 (first published as IEEE Early Access
 * Article, July 2017, Digital Object Identifier: 10.1109/TNET.2017.2720172).
 * 
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH
 * THE SOFTWARE.
 */
package transformer;

import java.util.*;

import common.APComputer;
import common.BDDACLWrapper;
import common.FWDAPSet;
import jdd.bdd.BDD;
import jdd.bdd.debug.DebugBDD;

public class IPinIP {

    static BDDACLWrapper bddengine;

    public static void set_bdd_engine(BDDACLWrapper engine)
    {
        bddengine = engine;
    }

    boolean encapsulator;
    /**
     * 
       currently only support at most two layers of IP header,
       for more than two layers of IP header, the operations will be more complicated, 
       though the principle is the same.
     **/ 

    // the guard includes field bit
    HashMap<Integer, Integer> encapsulations;
    int encapsulator_guard_union;
    //int encapsulator_guard -> int encapsulated_header;

    boolean decapsulator;
    // the guard  includes field bit
    int decapsulator_guard;
    int header_filters;

    // atomic predicate -> transformed predicate
    HashMap<Integer, Integer> predicatesMap;
    HashSet<Integer> computedPredicates;
    
    HashMap<Integer, FWDAPSet> transformationMap;

    public IPinIP()
    {
        encapsulator = false;
        decapsulator = false;
    }

    public void add_encapsulator(int guard, int header)
    {
        if(encapsulator)
        {
            encapsulations.put(guard, header);
            BDD thebdd = bddengine.getBDD();
            encapsulator_guard_union = thebdd.orTo(encapsulator_guard_union, guard);

        }else
        {
            encapsulator = true;
            encapsulations = new HashMap<Integer, Integer> ();
            encapsulations.put(guard, header);

            BDD thebdd = bddengine.getBDD();
            // increase ref for encapsulator_guard_union
            thebdd.ref(guard);
            encapsulator_guard_union = guard;

            //((DebugBDD) thebdd).check_node(encapsulator_guard_union, "encapsulator guard union");

        }
    }
    
    public void add_encapsulator_update(int guard, int header)
    {
        if(encapsulator)
        {
            encapsulations.put(guard, header);
            BDD thebdd = bddengine.getBDD();
            encapsulator_guard_union = thebdd.orTo(encapsulator_guard_union, guard);

        }else
        {
            encapsulator = true;
            encapsulations = new HashMap<Integer, Integer> ();
            encapsulations.put(guard, header);

            BDD thebdd = bddengine.getBDD();
            // increase ref for encapsulator_guard_union
            thebdd.ref(guard);
            encapsulator_guard_union = guard;

            //((DebugBDD) thebdd).check_node(encapsulator_guard_union, "encapsulator guard union");

        }
        
        computedPredicates = null;
        predicatesMap = null;
    }

    public void add_decapsulator(int guard, int headerfilter)
    {
        if(decapsulator)
        {
            BDD thebdd = bddengine.getBDD();
            int tmp = thebdd.ref(thebdd.or(decapsulator_guard, guard));
            thebdd.deref(decapsulator_guard);
            decapsulator_guard = tmp;
            
            header_filters = thebdd.orTo(header_filters, headerfilter);
            
        }else
        {
            decapsulator = true;
            decapsulator_guard = guard;
            header_filters = headerfilter;
        }
    }
    
    public void add_decapsulator_update(int guard, int headerfilter)
    {
        if(decapsulator)
        {
            BDD thebdd = bddengine.getBDD();
            int tmp = thebdd.ref(thebdd.or(decapsulator_guard, guard));
            thebdd.deref(decapsulator_guard);
            decapsulator_guard = tmp;
            
            header_filters = thebdd.orTo(header_filters, headerfilter);
            
        }else
        {
            decapsulator = true;
            decapsulator_guard = guard;
            header_filters = headerfilter;
        }
        
        computedPredicates = null;
        predicatesMap = null;
    }

    // only encapsulate dst ip field, for irrelevant pkts, output them as they are
    public int perform_encapsulation(int in_pkt)
    {
        BDD thebdd = bddengine.getBDD();

        if(encapsulator)
        {
            //System.out.println("in encapssulator:" + in_pkt);

            int out_pkt = BDDACLWrapper.BDDFalse;
            int remain_pkt = bddengine.diff(in_pkt, encapsulator_guard_union);

            if(remain_pkt == in_pkt)
            {
                //thebdd.deref(remain_pkt);
                return in_pkt;
            }

            for(int guard : encapsulations.keySet())
            {
                int to_be_encapped = thebdd.ref(thebdd.and(guard, in_pkt));

                if(to_be_encapped != BDDACLWrapper.BDDFalse){

                    int encapped = bddengine.push_inner_ipdst(to_be_encapped, encapsulations.get(guard));
                    out_pkt = thebdd.orTo(out_pkt, encapped);
                    thebdd.deref(to_be_encapped);
                    thebdd.deref(encapped);
                }
                //System.out.println("perform encapsulation");
            }
            out_pkt = thebdd.orTo(out_pkt, remain_pkt);

            thebdd.deref(remain_pkt);
            //System.out.println("out:"+out_pkt);
            return out_pkt;
        }else{
            thebdd.ref(in_pkt);
            return in_pkt;
        }

    }

    // only de-encapsulate dst ip field, for irrelevant pkts, output them as they are
    public int perform_decapsulation(int in_pkt)
    {
        BDD thebdd = bddengine.getBDD();
        if(decapsulator)
        {
            int out_pkt = BDDACLWrapper.BDDFalse;
            int remain_pkt = bddengine.diff(in_pkt, decapsulator_guard);

            if(remain_pkt == in_pkt)
            {
                //thebdd.deref(remain_pkt);
                return in_pkt;
            }

            int to_be_decapped = thebdd.ref(thebdd.and(in_pkt, decapsulator_guard));
            out_pkt = bddengine.pop_outer_ipdst(to_be_decapped);
            
            out_pkt = thebdd.andTo(out_pkt, header_filters);
            
            out_pkt = thebdd.orTo(out_pkt, remain_pkt);

            thebdd.deref(remain_pkt);
            thebdd.deref(to_be_decapped);

            return out_pkt;
        }else{
            thebdd.ref(in_pkt);
            return in_pkt;
        }

    }

    public int ForwardAction(int input_pkts)
    {
        int tmp1 = perform_decapsulation(input_pkts);
        int out_pkts = perform_encapsulation(tmp1);

        bddengine.deref(tmp1);

        return out_pkts;
    }
    
    public FWDAPSet ForwardAction(FWDAPSet input_pkts)
    {
        FWDAPSet transformed_set = new FWDAPSet(BDDACLWrapper.BDDFalse);
        FWDAPSet out_set = new FWDAPSet(input_pkts);
        
        for(int ap : transformationMap.keySet())
        {
            if(input_pkts.contains(ap))
            {
                out_set.remove(ap);
                transformed_set.union(transformationMap.get(ap));
            }
        }
        
        out_set.union(transformed_set);
        
        return out_set;
    }
    
    public void updatePredicatesMap(APComputer apc)
    {
        if(predicatesMap == null)
        {
            predicatesMap = new HashMap<Integer, Integer> ();
            computedPredicates = new HashSet<Integer> ();
        }
        
        for(int ap : apc.getAllAP())
        {
            if(!computedPredicates.contains(ap))
            {
                computedPredicates.add(ap);
                int out_pkts = ForwardAction(ap);
                if(ap == out_pkts)
                {
                    // no change
                    bddengine.deref(ap);
                }else
                {
                    predicatesMap.put(ap, out_pkts);
                }
            }
        }
    }
    
    public void setaps(APComputer apc)
    {
        HashSet<Integer> aps = apc.getAllAP();
        transformationMap = new HashMap<Integer, FWDAPSet>();
        
        for(int predicate : predicatesMap.keySet())
        {
            if(aps.contains(predicate))
            {
                int after = predicatesMap.get(predicate);
                HashSet<Integer> rawset = apc.getAPExpComputed(after);
                if(rawset == null)
                {
                      System.err.println("bdd expression not found!");
                      System.exit(1);
                }else
                {
                      FWDAPSet apset = new FWDAPSet(rawset);
                      transformationMap.put(predicate, apset);
                }
            }
        }
    }

}
